D:Dsys, rx, ra, rt:(IdId).
Inj(Id; Id; rx)  Inj(Id; Id; ra)  Inj(Id; Id; rt)  d-rename(rx;ra;rt;D)  Dsys 

latex

Definitions	Dsys, d-rename(rx;ra;rt;D), ma-rename(rx;ra;rt;M), P  Q, Inj(A; B; f), x:A. B(x), t  T, Id
Lemmas	Id wf, inject wf, ma-rename wf, dsys wf